$\forall$${\it the\_w}$:World, $l$:IdLnk, ${\it mss}$:(Msg List). withlnk($l$;${\it mss}$) $\in$ (($t$:Id $\times$ (${\it the\_w}$.M($l$,$t$))) List)